ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
a:((k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)T)), snd:msg-spec(ds;da), l:IdLnk.
x  dom(ds)
 ecl-m3(a;snd;x;l)
  k:{k:Knd| (k  ks) }(tg:{tg:Id| (tg  ecl-tags(l;snd)) }
  k:{k:Knd| (k  ks) }((State(ds  x : T)Valtype(da;k)
  k:{k:Knd| (k  ks) }(((da(rcv(l,tg))?Void List))) List 

latex

Definitions

t  T, x:A. B(x), P  Q, False, A, AB, , x:A. B(x), Top, IdDeq, x : v, b, b, , Prop, Type, x.A(x), x. t(x), a:A fp B(a), x  dom(f), P & Q, P  Q, Unit, left+right, f  g, f(a), Atom$n, msg-spec(ds;da), x:A. B(x), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, let x,y,z = a in t(x;y;z), map(f;as), let x = a in b(x), ecl-m3(a;snd;x;l), nil, <a,b>, IdLnkDeq, KindDeq, IdLnk, Knd, product-deq(A;B;a;b), f(x)?z, Void, rcv(l,tg), type List, Valtype(da;k), x:AB(x), State(ds), , x:AB(x), Id, ecl-tags(l;snd), (x  l), {x:A| B(x) }, s = t, ||as||, f(x), A & B, a<b, EqDecider(T), s ~ t, {T}, SQType(T), xL. P(x), 2of(t), 1of(t), msg-item(ds;da;k;l), P  Q, S  T

Lemmas

subtype rel list, l member subtype, member-ecl-tags, list-set-type2, pi2 wf, pi1 wf, msg-item wf, product-deq wf, idlnk-deq wf, deq wf, IdLnk wf, msg-spec wf, fpf wf, let wf, map wf, nat wf, ecl-tags wf, ifthenelse wf, l member wf, ma-valtype wf, Knd wf, Kind-deq wf, rcv wf, nat properties, decl-state wf, subtype rel dep function, fpf-join wf, fpf-cap wf, fpf-cap-join-subtype, fpf-join-cap-sq, fpf-single wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, fpf-cap-single1, Id wf, id-deq wf, subtype rel self